A:Type, eq:EqDecider(A), B:Top, f:a:A fp Top. f ||  

latex

Definitions	False, b, x  dom(f), , t  T, x. t(x), x:A. B(x), Top, Prop, P & Q, x(s), P  Q, f || g, EqDecider(T), a:A fp B(a)
Lemmas	fpf wf, top wf, deq wf, assert wf, fpf-dom wf, fpf-empty wf